Online Shopping Example

Online Shopping Example

In this example, buyer communicates with the seller through the service channel B2S to invoke its service, while channel Bch is a private channel for the following session only. In the Session, the buyer firstly sends a message QuoteRequest through channel Bch to the seller. The seller responds with some quotation value x, which is a variable.

First of all, we need to declare the service channels to be used in the choreography or orchestration. If a service channel is used without declaration, it will fail the parser.

channel B2S ; //The pre-established channel between the buyer and the seller
channel S2H ; //The pre-established channel between the seller and the shipper

The following is the specification of choreography.

Chor cBuySell {

Main() = B2S(Buyer, Seller, {Bch}) -> Bch(Seller, Buyer, Ack) -> Session();
   Session() = Bch(Buyer, Seller, QuoteRequest) ->
                     Bch(Seller, Buyer, QuoteResponse.x) ->
                     if (x <= 1000) {
                             Bch(Buyer, Seller, QuoteAccept) ->
                             Bch(Seller, Buyer, OrderConfirmation) ->
                             S2H(Seller, Shipper, {Bch, Sch}) ->
                             (Sch(Shipper, Buyer, DeliveryDetails.y) -> Stop ||| Bch(Shipper, Seller, DeliveryDetails.z) -> Stop)
                     } else {
                            Bch(Buyer, Seller, QuoteReject) -> Session() [] Bch(Buyer, Seller, Terminate) -> Stop
                   };

}

The choreography coordinates three roles (i.e.,Buyer, Seller and Shipper) to complete a business transaction. At line 1, the Buyer communicates with the Seller through service channel B2S to invoke its service. Channel Bch which is sent along the service invocation is to be used as a session channel for this session only. In the Session, the Buyer firstly sends a message QuoteRequest to the Seller through channel Bch. At line 3, the Seller responds with some quotation value x, which is a variable. Notice that in choreography, the value of x may be left unspecified at this point. At line 7, the Seller sends a message through the service channel S2H to invoke a shipping service. Notice that the channel Bch is passed onto the Shipper so that the shipper may contact the Buyer directly. At line 8, the Shipper sends delivery details to the Buyer and Seller through the respective channels. The rest is self-explanatory.

The following is the implementation of the orchstration. Each role is implemented as a separate component. Each component contains variable declarations (optional) and process definitions. We assume that the process Main defines the computational logic of the role after initialization. We remark that the orchestration generally contains more details than the choreography, e.g., the variable counter in Buyer constraints the number of attempts the buyer would try before giving up.

Orch oBuySell {
Role Buyer {
    var counter = 0;
    Main () = (counter = 0) -> B2S!{Bch1} -> Bch1?Ack -> Session();

    Session() = Bch1!QuoteRequest -> (counter = counter+1) ->
                      Bch1?QuoteResponse.x ->
                      if (x <= 1000) {
                                Bch1!QuoteAccept ->
                                Bch1?OrderConfirmation ->
                                Bch1?DeliveryDetails.y ->  Stop
                      } else {
                                if (counter <= 3) {
                                         Bch1!QuoteReject -> Session()
                                } else {
                                         Bch1!Terminate -> Main
                                }
                      };
}
}

Role Seller[1] { // the size of the role gives the number of threads that can be forked for the service invocations. If this number is bigger, the more number of service can be invoked concurrently.
    var x = 1200; //the quotation
    Main = B2S?{ch} -> ch!Ack -> Session();

    Session() = ch?QuoteRequest ->
                      ch!QuoteResponse.x ->
                      (
                             ch?QuoteAccept ->
                             ch!OrderConfirmation ->
                             S2H!{ch,Sch} ->
                             Sch?DeliveryDetails.y -> Stop
                      []
                             (ch?QuoteReject -> Session() [] ch?Terminate -> Stop)
                      );

}

Role Shipper[1] {
    var detail = 2010; //the delivery detail
    Main() = S2H?{ch1,ch2} ->
                 (ch1!DelieryDetails.detail -> Stop ||| ch2!DelieryDetails.detail -> Stop);
    }

}

Some properties that can be checked are the following:

#assert oBuySell deadlockfree;
#assert oBuySell refines cBuySell;
#define inv Buyer1.counter <= 4;
#assert oBuySell |= []inv;
#assert oBuySell |= []<> inv;

#assert oBuySell reaches inv;